Nuprl Lemma : insert_wf
0,22
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
a
:
T
,
L
:
T
List. insert(
a
;
L
)
T
List
latex
Definitions
insert(
a
;
L
)
,
if
b
t
else
f
fi
,
deq-member(
eq
;
x
;
L
)
,
EqDecider(
T
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
deq
wf
,
deq-member
wf
,
ifthenelse
wf
origin
T:Type, eq:EqDecider(T), a:T, L:T List. insert(a;L) 
T List T:Type, eq:EqDecider(T), a:T, L:T List. insert(a;L) T List 
t else f fix:A. B(x) T